$\forall$$T$:Type, $d$:EqDecider($T$), $x$,$y$:$T$. ($x$ = $y$) $\Leftarrow\!\Rightarrow$ ($\uparrow$(eqof($d$)($x$,$y$)))